COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	-------------------------------------------------------------------------
C00006 00003	Title: Basic Research in Artificial Intelligence
C00020 ENDMK
C⊗;
-------------------------------------------------------------------------

? 	Not all precise human reasoning follows the format of mathematics.
? One difference is that human reasoning often depends on observation at
? every stage.  In order to study this, Filman (1977) has formalized the
? reasoning involved in a chess problem that requires retrospective
? analysis.  Some of the important facts can be formalized as mathematical
? theorems about legal chess moves, but much of the reasoning depends on
? direct observation of what may be called "partial chess boards".  Filman's
? proof is still far too long, from which we conclude that we don't yet
? understand this kind of human reasoning.


There is a large connection between between the epistemologial problems
stated above and our work on proof-checking.  The question of how
derivations, rather than facts about the world, can be properly
represented is the same problem but asked about the reasoning problem
itself.  The ability to construct a proof checker which accepts proofs at
the same level of detail as a human and can fill in the gaps if asked,
would be de facto evidence that we are representing reasoning processes
with reasonable accuracy.  In this sense we view the proof checker as a
testing ground for our epistemological ideas in two ways.  One is we can
test whether the formalizations of facts about the world we discuss above
can be used the conclude the desired information.  Second is whether we
are getting the structure of the derivations correct by comparing the
machine checked versions to our informal ones.

Thus we have tried to construct FOL in such a way as to reflect our 
epistemological ideas about derivations.  This work has largly not been 
described in publications and one goal of ours is to write about this 
aspect of the FOL project.  The most important feature to be discussed is
the semantic attachment mechanism.  This is a device that allows a user
to construct a model of his theory and then observe the behavior of the
model to determine facts, rather than deduce them from axioms.  It is this 
feature that we mentioned above was used agressively by Filman to do 
study reasoning using chess problems.  
-------------------------------------------------------------------------
Title: Basic Research in Artificial Intelligence

	This is a request for a continuing grant of xxx per year
in support of basic research in artificial intelligence
with emphasis on the structure of formal reasoning and
computer proof checking.  The computer proof checking supports the
basic research in AI, but also has applications to verifying
computer programs and is independently valuable.


Introduction

	Artificial intelligence has proved to be a difficult branch
of science.  Some people thought that human level intelligence
could be achieved in ten or twenty years, but this was based on
the difficulties they could see when they made the optimistic
predictions.  Our own opinion is that major scientific discoveries
remain to be made.
Moreover, many of these discoveries require theoretical advances and
not merely the extension of current ideas for producing "expert programs"
to new domains.
The increasing emphasis by ARPA and other agencies sponsoring AI
research on immediate applications has resulted in a serious
imbalance.  Deciding what the basic issues are is difficult
enough without having formulate everything in terms of demonstration
programs to be available in two years.

	Our research is based on the idea that for many purposes,
the problems of artificial intelligence can be separated into two
parts - an epistemological part and a heuristic part.
The %2epistemological%1 part concerns what facts and inference
rules are available for solving a problem and how they can be
represented in the memory of a computer, and the heuristic part
concerns procedures for deciding what to do on the basis of the
necessary facts.  Most work in AI has concerned the %2heuristics%1,
and computer representations of information have been chosen that
are capable of representing only a part of the information that
would be available to a human.  The modes of reasoning used by
present programs are often even weaker than the representations
themselves.

	The lines of research we plan to pursue are exemplified in
the attached reprints and preprints.  Here we shall explain how this
work fits together.  Our long range goal is a program that can be told
facts about the world and can use them effectively to achieve the
goals it is given.
Sometimes it will use the facts directly from its data base using
deductive and inductive processes like the deductive processes
of mathematical logic.  However, we are already sure, (McCarthy 1977a),
that conjectural processes will be needed that go beyond deduction
as preently conceived.  Sometimes it will use these facts to compile
"expert programs" that use these facts in a more efficient way than
simple reasoning.  However, the expert programs will have to defer
to reasoning when unexpected use of he factual data-base is required.

	We do not propose to implement such a program immediately -
maybe not at all within the next five years.  This is because its
success depends on successful formalization of facts about the world.
We have made progress in this formalization, but we may be occupied
with it exclusively for the forseeable future.  In short we will
emphasize theoretical artificial intelligence except for the work
with proof-checkers to be described below.

	The main areas of our previous accomplishment and future work
are the following (as now seen):

.item← 0

#. Development of %2circumscription%1 as a mode of reasoning and its
application to artificial intelligence.  %2Circumscription%1 formalizes
the process of concluding (often incorrectly) that a certain collection
of facts is all that are relevant for solving a problem.  It does this
by allowing one to formally assume that the entitities that are generated
by specified processes are all the entities of a specified kind.
This is common in human reasoning and, for reasons described in the preprint,
canot be accomplished by any form of deduction.

#. Development of treating concepts as objects.  This, described in
(McCarthy 1977b),
facilitates, and may be required for, reasoning about knowledge, belief,
wants, possibility and necessity.

#. The current biggest gap in computer reasoning about the physical world
is the complete lack of a system for reasoning about concurrent processes.
All the current problem solving programs assume that each action of the
program produces a next state that depends on the current state, the action,
and sometimes on a random variable.  They don't take into account continuous
processes or the fact that other actions and events may be taking place.
We believe that circumscription may be important in formalizing what
people know about such processes.

#. We also plan some study of the theory of patterns, especially higher
order patterns in which function variables may be matched and relations
between patterns - for example, the relation between a pattern describing
a type of three-dimensional object such as a person or a vehicle and its
patterns of its perception - such as its projection on a retina as modified
by angle of vision, lighting and occlusion by other objects.

	In all this work, the emphasis is on representation of the information
that is actually available to an observer with given opportunities to
observe and compute.


PROOF CHECKING BY COMPUTER

	We must distinguish theorem proving by computer from proof-checking
by computer.

	It is an essential part of the notion of proof in a formal
system that a candidate proof can be checked by a mechanical process.
It is a consequence of the work of Goedel, Church and Turing that
no mechanical process can always determine whether a proof of a
given sentence exists in a formal system.
In principle, therefore, proof-checking should be easy, while all
the difficulties of understanding the creative processes of a
mathematician are involved in making a high powered theorem prover.

	However, in spite of the simplicity of modern logical and set
theoretic systems and the brevity with which they permit axiomatizing
mathematical and physical systems, checking actual proofs
has encountered formidable difficulties.  It is easy enough to make
proof-checkers for the formal systems in logic and set theory textbooks,
and we have done it.  The difficulty is that the formal proofs of easy
theorems turn out to be ten times longer than informal proofs, and the
excess in length grows the further one advances into the theory.  The
trouble is that mathematicians have not succeeded in completely formalizing
the languages and reasoning processes they actually use.  Much reasoning
that at first seems to be within a given mathematical system, actually is
metamathematical reasoning about the system.  Even when a mathematician
is working within a system, he establishes shortcuts whose repeated use
keeps down the length of a proof.

	We have a proof-checker called FOL (for first order logic) (Weyhrauch
1977a), we have been improving it since 1973, and we propose to improve
it further under this grant.  (Rewriting it from scratch will be required
at some point, but we aren't sure when this will be the best use of
limited manpower).  With FOL, we have checked a variety of mathematical
proofs, and each such project has told us something about how to improve
the proof-checker or how to formalize a given mathematical domain or
how to write and debug proofs.  Here are some of the more significant proofs.

[Richard, put in about 30 lines here]

	Recent improvements have reduced the length of some proofs by
a factor of better than ten.  Here are some of them and what they have
accomplished.

[Richard, 40 lines]

	Not all precise human reasoning follows the format of mathematics.
One difference is that human reasoning often depends on observation at
every stage.  In order to study this, Filman (1977) has formalized the
reasoning involved in a chess problem that requires retrospective
analysis.  Some of the important facts can be formalized as mathematical
theorems about legal chess moves, but much of the reasoning depends on
direct observation of what may be called "partial chess boards".  Filman's
proof is still far too long, from which we conclude that we don't yet
understand this kind of human reasoning.

	Our plans for FOL include the following:

[Richard, 100 lines].